$\forall$$i$, $x$, $a$:Id, $A$, $T$:Type, $x_{0}$:$A$, $P$:($A$$\rightarrow$$T$$\rightarrow$Prop). R{-}pre{-}init1($i$;$x$;$A$;$x_{0}$;$a$;$T$;$P$) $\in$ Realizer